Restructure the PoC engine into two passes that reuse a concrete trace,
and document the target architecture.

- concrete_trace(): run with the input substituted in (deterministic, no
  fork) and harvest the ordered rule ids from the rewrite logs.
- trace(): replay symbolically, selecting each branch by matching rule
  ids against the concrete trace instead of an SMT/simplify call per
  candidate.
- rewrite the unit test around the new branch-matching / log-extraction
  helpers; refresh the README architecture + flow diagrams.
- add DESIGN.md: the remainder-driven DART loop (ck/rk), the chosen
  Haskell guided-step backend feature, and the v0 -> v3 milestones.

Replace post-hoc condition negation with backend-provided sibling
predicates (the remainder rk), realizing the remainder-driven DART loop
on the existing execute RPC (no backend change required).

- PathConstraint gains `siblings`: the rule_predicate of each non-chosen
  successor at a branch node (the rk alternatives).
- trace() records ck (chosen) + rk (siblings) at each branch; _match_branch
  now returns the sibling successors alongside the chosen one.
- diverging_inputs() replaces flipped_inputs(): for each branch node i and
  each sibling rk, solve prefix_{<i} & rk; feasible models are new inputs,
  infeasible siblings are pruned. Handles multi-way branches correctly.
- add a two-branch IMP integration test asserting exactly the 3 feasible
  leaves are found and the UNSAT combination is never generated.
- refresh README diagrams and DESIGN status accordingly.

Verified: 7 unit + 8 integration (legacy + Booster) pass; black/isort/
flake8/autoflake/mypy clean.

A skipif-guarded (CONCOLIC_BENCH=1) benchmark over a scaling family of
branchy IMP programs. Instruments the engine's execute / get_model calls
to measure where exploration time goes.

Measured (Booster, K v7.1.322): forward-replay `execute` is 97-98% of
wall time across k=1..6 and grows ~O(k^2) in branching calls, while
diverging-input `get_model` is ~1-2% and shrinks. This justifies the
Haskell guided-step optimization, which targets the forward-replay cost.

Thread the optional `assume-remainder-unsat` execute flag from the
concolic engine's forward replay down to the Kore RPC request.

- KoreClient.execute: new optional `assume_remainder_unsat` param
  (omitted from the request when None; ignored by backends that lack it).
- ConcolicEngine: new `assume_remainder_unsat` option (default True),
  passed on every replay `execute`. On a backend that supports the flag
  this skips the per-branch remainder-feasibility SMT identified as
  ~97% of replay time by the benchmark.

End-to-end verified against a locally-built kore-rpc-booster carrying the
flag: a rule with a satisfiable remainder aborts with the flag off and
proceeds (stuck/finished) with it on; concolic still finds all feasible
paths. Existing tests pass against the stock binary (flag ignored).